\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Cmd}$:Type, ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it In}$:AbsInterface(${\it Cmd}$), ${\it Out}$:AbsInterface(Top),\+
\\[0ex]${\it Sys}$:AbsInterface(${\it Cmd}$ List).
\-\\[0ex](E(${\it In}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ \=($\forall$$f$:sys{-}antecedent(${\it es}$;${\it Sys}$).\+
\\[0ex]($\forall$$u$:E(${\it Sys}$). ($f$($u$) = $u$ $\in$ E) $\Leftarrow\!\Rightarrow$ ($\uparrow$($u$ $\in_{b}$ ${\it In}$)))
\\[0ex]$\Rightarrow$ fifo{-}antecedent(${\it es}$;${\it Sys}$;$f$)
\\[0ex]$\Rightarrow$ input{-}forwarding\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Sys}$; ${\it isupdate}$; ${\it In}$; $f$)
\-\\[0ex]$\Rightarrow$ \=($\forall$${\it chain}$:(E(${\it Sys}$)$\rightarrow$(Id List)).\+
\\[0ex]chain{-}consistent($f$;${\it chain}$)
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E(${\it Sys}$).\+
\\[0ex]filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; $e$))
\\[0ex]=
\\[0ex]${\it In}$(updates(cr{-}explanation\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Sys}$; $f$; $e$)))
\-\\[0ex]$\in$ (${\it Cmd}$ List))))
\-\-\-
\end{tabbing}